COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	∂AIL Robert L. Ashenhurst↓The University of Chicago↓5640 South Ellis
C00006 ENDMK
C⊗;
∂AIL Robert L. Ashenhurst↓The University of Chicago↓5640 South Ellis
↓Chicago, IL 60637∞
.<<312 753-8762>>

Dear Bob:

	The following is for the Technical Correspondence section
 of the %2Communications%1.

.bb The Prospects for Program Verification

	The prospects are better than De Millo, Lipton and Perlis
think for the following reasons.
.item←0

	#. It is already possible to give a programming problem with
a requirement for a proof of correctness as one problem on a midterm
examination and get reasonably good scores from students more interested
in programming than verification.
The following problem is taken from Fall 1977 the final examination of Computer
Science 206 at Stanford University.

1. %2rev x%1 is the "reverse" of the arbitrary S-expression %2x%1.  Thus
%2rev%1 (A.(B.C)) = ((C.B).A).  Note that %2rev%1 applied to a list
does not give the usual reversal of the list.

	a. Write a recursive definition of %2rev%1.

	b. Prove that %2rev%1 is total.

	c. Prove that %2rev%1 satisfies %2∀x: rev rev x = x%1.

As I recall, more than half of the students got this problem correct, and
grading it was rather like grading any other mathematics problem; the
good solutions, a few quite different from what was expected, were a
pleasure to read.

	#. The length in characters of the set of commands for our
interactive theorem prover to verify a program for computing the
set of partitions of a list is about xx times the number of characters
in the progam.  Admittedly this program is still in the toy category.
but we expect the ratio to hold for more complex programs and even
to improve as larger and larger parts of the proof become doable
automatically.

	#. The correctness of a program is not always a single statement.
Very often, one has a number of somewhat independent statements that
whose proof would improve one's confidence.

	#. When a subjectively small change is made in a program, a
correspondingly small change should be required in the file commands to
to the program verifier.